Nuprl Definition : es-p-le
11,40
postcript
pdf
e
p
e'
==
e
p
<
e'
(
e
=
e'
)
latex
clarification:
es-p-le(
es
;
p
;
e
;
e'
) == es-p-locl(
es
;
p
;
e
;
e'
)
(
e
=
e'
es-E(
es
))
latex
Definitions
P
Q
,
e
p
<
e'
,
s
=
t
,
E
FDL editor aliases
es-p-le
origin
e' == e p< e' 
(e = e')
(e = e' 
es-E(es)) e' == e p< e' (e = e')
(e = e' es-E(es)) Q